$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:ES, $x$:Id, $e$:\{$e$:E$\mid$ @loc($e$)($x$:$T$)\} , ${\it e'}$:E.
\\[0ex](((${\it e'}$ $<$loc $e$) \& ($\neg$(($x$ when ${\it e'}$) = ($x$ when $e$) $\in$ $T$))
\\[0ex]\& $\forall$${\it e''}$$\in$[${\it e'}$,$e$).($x$ after ${\it e''}$) = ($x$ when $e$) $\in$ $T$)
\\[0ex]$\vee$ (${\it e'}$ = $e$ \& ($\forall$${\it e''}$$<$$e$. ($x$ after ${\it e''}$) = ($x$ when ${\it e''}$) $\in$ $T$)))
\\[0ex]$\Rightarrow$ (lastchange($x$;$e$) = ${\it e'}$)